$\forall$$p$:(IdLnk List), $i$:\{0..$\parallel$$p$$\parallel^{-}$\}, $j$:\{0..($i$+1)$^{-}$\}. \\[0ex]lpath($p$) $\Rightarrow$ lconnects(l\_interval($p$;$j$;$i$);source($p$[$j$]);source($p$[$i$]))